$\forall$$w$:World, $e$:E. \\[0ex]FairFifo \\[0ex]$\Rightarrow$ rcv?($e$) \\[0ex]$\Rightarrow$ (msg(lnk(kind($e$));tag(kind($e$));val($e$)) $\in$ m(loc(sender($e$));time(sender($e$))))